Inference at * 1 3 1 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
  P(n) 

latex

 by InteriorProof (CompNatInd (-1)) 

latex

 1: 

 1: 4. n1:. (n1 < n)  (P(n1))
 1:   P(n)
 .

Definitions	, , False, A, A  B, i  j , P  Q, t  T, x:A. B(x)
Lemmas	le wf, nat wf, ge wf, nat properties